; REQUIRES: cocoa
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic QF_FF)

(declare-const b Bool)
(declare-const c Bool)
(declare-const a Bool)
(declare-const out (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _11 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _10 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _1 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _0 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _6 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _3 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(declare-const _2 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
(assert
	(not (=> (and (and (= _1 (ite b #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= _2 (ite c #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= _0 (ite a #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513))) (and (= (ff.mul _0 _0) _0) (= (ff.mul _1 _1) _1) (= (ff.mul _2 _2) _2) (= (ff.mul (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1) (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1)) _3) (= (ff.mul (ff.add (ff.mul _3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) _2) (ff.add _2 (ff.mul _3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.mul _6 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= (ff.mul _0 _6) _10) (= (ff.mul (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1) _11) (= (ff.add _10 _11) out))) (and (or (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 out) (= #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513 out)) (= (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 out) (ite a (=> (not (= b a)) c) b)))))
)
(check-sat)
